\setcounter{secnumdepth}{-1}
\chapter{Research description}

\section{Overview of the Main Goals}
\label{rd:ov}

The initial goal of this research was to develop the \K semantics of a core of OCL (Object Constraint Language) according to OMG standard, version 2.3. The purpose was to define both the static parts of OCL (corresponding to well-formedness constraints and queries over UML models) and the dynamic parts (corresponding to pre/post conditions of methods). The dynamic part of OCL involves symbolic execution of methods using OCL annotations given as pre/post conditions. The results obtained when developing symbolic execution encouraged the idea of designing a generic symbolic execution framework for languages using \K. So, the central aims of this research are the following:
\begin{itemize}
\item {\it Support for symbolic execution in \K framework}. This involves adding symbolic values to existent \K builtins and creating a mechanism for generating such values. Also, we need to offer the user the possibility to define its own symbolic values which may consist in symbolic pieces of programs. The support for symbolic execution must be provided together with its own well-defined theoretical background.
\item {\it Applications of symbolic execution}. Since the symbolic execution is meant to be general, we need to create a range of applications in order to prove that the support we offer is generic. This goal is linked with the first one in the sense that most of the development of the support itself is driven by creating applications which use symbolic execution. This allows to find a clear distinction between language independent and language specific aspects of symbolic execution. A subgoal would be to redefine the dynamic part of OCL using the new approach and to test it on modeling languages.
\item {\it Implementing deductive systems over \K symbolic executions}. This goal consists in implementing existent deductive systems (e.g. Reachability Logic) together with specific theories depending on the application needs (e.g. heap, cache, arrays, ...) 
\end{itemize}



\section{Proposed approach}

As already stated in the previous section the main goal of the research is to add support for symbolic execution to the \K framework. In order to achieve this goal, there are a few important steps to follow:
\begin{itemize}
\item Learning the architecture of \K framework, in order to be able to add support for symbolic execution into it. Also, provide some formal background for symbolic execution such that it extends the existent \K formalism.
\item Investigate some applications of symbolic execution by extracting the common aspects which should be offered as support by \K and also isolate the language or domain specific aspects related to symbolic execution.
\item Investigate the most recent work done on deductive systems and design a way to integrate them into \K as well.
\end{itemize}

The steps described above are general and cover the whole subject of this research. 
